A:Type, eq:EqDecider(A), f, g:a:A fp Top, L:A List.
l_disjoint(A;1of(f  g);L)  l_disjoint(A;1of(f);L) & l_disjoint(A;1of(g);L) 

latex

Definitions	P  Q, 1of(t), t  T, P  Q, x:A. B(x), l_disjoint(T;l1;l2), Prop, P & Q, Top, P  Q, x. t(x), EqDecider(T), a:A fp B(a), f  g, x  dom(f), b, P  Q, (x  l), False, A, {T}
Lemmas	pi1 wf, l member wf, fpf-join-dom, assert wf, fpf-dom wf, fpf wf, deq wf, l disjoint-fpf-dom, fpf-join wf, top wf, l disjoint wf